Book Chapter
Learning-Guided Higher-Order Automated Reasoning for Isabelle/HOL
Jan Jakubův, Cezary Kaliszyk, Martin Suda
Lecture Notes in Computer Science | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Springer Nature Switzerland | Published : 2027
Abstract
We present higher-order versions of ENIGMA and Deepire, the two prominent learning-guided reasoning systems extending saturation-based automatic theorem provers E and Vampire, respectively. We evaluate these on a large Isabelle/HOL corpus, which emulates their use in Sledgehammer, and observe consistent improvement. Stress-testing the Sledgehammer export revealed several bugs, both in the provers and in Sledgehammer itself, which were all fixed for the final evaluation.